COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	\input jmclet
C00004 ENDMK
C⊗;
\input jmclet
\jmclet
\address
Professor Carlo H. S\'equin
Computer Science Department
571 Evans Hall
University of California
Berkeley, CA  94720
\body

	Dear Professor S\'equin:

	I just noticed your letter of February 10 in a
stack of mail that had been put aside.  In case it is
still relevant I enclose my comments about Shankar's work.

	Dr. Shankar worked in the Formal Reasoning Group
on a two year appointment as Research Associate since he
received his PhD at the University of Texas in 1986.

	In my opinion his thesis work on making the Boyer-Moore
theorem prover accept a proof of the Goedel incompleteness
theorem and his previous computer assisted proof of the
Church-Rosser theorem constitute the most ambitious and
successful computer-checked mathematical proof that has
been done.  It still hasn't been equalled.

	While at Stanford he has worked on an improved
logic of computer programs and developed ideas of improved
interactive theorem provers.  In both of these areas he
has promising results.

\closing
Sincerely,
John McCarthy
\endletter
\end